rv-disjoint(p;n;X;Y)
== i:{0..n}.
== (s1, s2:({0..n}Outcome). (j:{0..n}. ((j = i))  (s1(j) = s2(j)))  (X(s1) = X(s2)))
==  (s1, s2:({0..n}Outcome).
==  (j:{0..n}. ((j = i))  (s1(j) = s2(j)))  (Y(s1) = Y(s2))) 

latex

---

clarification:

rv-disjoint(p;n;X;Y)
== i:{0..n}.
== (s1:({0..n}p-outcome(p)), s2:({0..n}p-outcome(p)).
== (j:{0..n}. ((j = i  ))  (s1(j) = s2(j)  p-outcome(p)))  (X(s1) = X(s2)  ))
==  (s1:({0..n}p-outcome(p)), s2:({0..n}p-outcome(p)).
==  (j:{0..n}. ((j = i  ))  (s1(j) = s2(j)  p-outcome(p)))  (Y(s1) = Y(s2)  )) 

latex

Definitions	P  Q, x:AB(x), x:A. B(x), {i..j}, #$n, P  Q, A, , Outcome, s = t, , f(a)
FDL editor aliases	rv-disjoint